r, s:RngSig, f:(|r||s|). rng_chom_p(r;s;f)   

latex

Up	rings 1
Definitions of Statement	rng_chom_p(r;s;f)
Definitions	x f y, P & Q, rng_chom_p(r;s;f), , t  T, x:A. B(x)
Lemmas	rng sig wf, rng times wf, rng car wf, rng hom p wf